package scala.examples.fs;
import scala.collection.mutable.ListBuffer

trait Typers extends SyntaxIsMappable {
  object EmptyContextTyper extends Typer {
    def apply[a <: NameElement](s: Scope[a]): List[Type] = error("Unkown scope: "+s) // bug in typechecker: didn't respect the underbinder regime
  }
     
  trait Typer {
    // would like to factor this out, but that TypeBinderEnv would then have to be parameterised in the 
    // class it instantiates to extend the environment
    def apply[a <: NameElement](b : Scope[a]): List[Type]
    def extend[a <: NameElement](b : Scope[a], t : List[Type]) = new Typer { 
      def apply[b <: NameElement](w : Scope[b]): List[Type] =  trace("ctx lookup("+w+")", w match { case _ : b.type => t case _ => Typer.this.apply(w) })
    } 
    
    /**
     * @pre p.isPath
     */
    def ofPath(p: Term): Type = p match {
// TODO:  why can't I write this:  case Path(List(BoundElement(_, b: Scope[NameElement]))) => this(b)
// TODO: having cases Path(List(x)) and p: Path yields duplicate cases error.. BUG?
// TODO: check that the final AST satisfies that x.isPath implies x.isInstanceOf[Path] -- maybe this can be enforced in the 
// FieldSel class? (i.e., having an assert(!isPath)... or maybe even this.isPath implies this.isInstanceOf[Path] in Term?
      case path@Path(comps) => 
         comps match {  // TODO: should BoundElement's type parameter be covariant?
           case List(u: BoundElement[NameElement]) => this(u.scope)(u.scope.indexFor(u).get) // Path-Var
           case _ => val (p, name) = path.split // Path-Select
             member(SingletonType(p), name) match {
              case Some(MField(n, tp, _)) => tp
            }
         }     
      
      /*case FieldSel(p: Path, name) =>  // TODO: check that parser maintains term.isPath implies term.isInstanceOf[Path]
          member(SingletonType(p), name) match {
            case Some(MField(n, tp, _)) => tp
          }*/
    }
    
    /**
     * Lifts ofCheck to lists of terms&types
     */
    def ofCheckList(tms: List[Term], tps: List[Type]): Boolean = {
      (for(val (tm,tp) <- tms.zip(tps)) yield ofCheck(tm, tp)) forall(.==(true)) //.toList.foldLeft(true)((x,y) => x && y)
    }
    
    def ofCheck(tm: Term, tp: Type): Boolean = <:<(of(tm), tp)
    def ofExpand(p: Path): Type = ofPath(expand(p))
    
    def of(tm: Term): Type = tm match {
      case p if p.isPath => ofPath(p); SingletonType(Path_.fromTerm(p)) // Path
      case FieldSel(tm, name) => member(ofPath(tm), name) match {  // Select
        case Some(MField(n, tp, _)) => tp
      }
      case MethodCall(tm, name, actuals) => member(ofPath(tm), name) match {  // Method
        case Some(MMethod(n, formals, tp, _)) if ofCheckList(actuals, formals) => tp
      }  
      case New(tp) if wf(tp) && concreteMems(unfolds(tp)) => tp // New
      case Let(tp, v, u) if ofCheck(v, tp) => underBinder(u, List(tp)) { (tm: Term) => (.of(tm))  } // Let
    }

    //  like a "strict" monadic sequence (if the unit result occurs in the list, that will be 
    // the overall result)
    def unfoldsList(tps: List[Type]): Option[List[UnderBinder[Name, List[Member]]]] = {
      val l = new ListBuffer[UnderBinder[Name, List[Member]]]
      for(val tp <- tps) {
        unfolds(tp) match {
          case Some(ub) => l += ub
          case None => return None
        }
      }
      
      Some(l.toList)
    }
    
    def unfolds(tp: Type): Option[UnderBinder[Name, List[Member]]] = trace("unfolds("+tp+")", tp match {
      case TPUnit() => Some(UnderBinder.unit(Nil)) 
      case TypeSel(p, a) => member(SingletonType(p), a) match {
        case Some(m) => m match {case MType(_, Some(tp)) => unfolds(tp) // case TypeMemberUnapp(tp) => unfolds(tp): TODO: bug
          case MTrait(_, tp) => unfolds(tp)
          case _ => None}
        case None => None // unfolds-class & unfolds-type
      }
      case TypeSig(parents, members) => unfoldsList(parents).map(ub => merge(ub, members))           // unfolds-signature
      case _ => None
    })

    def member(tp: Type, n: String): Option[Member] = tp match {
      case SingletonType(p) => getMember(n, Some(p), unfolds(ofExpand(p))) // \ni-singleton
      case _ => getMember(n, None, unfolds(tp))                            // \ni-other
    }
    
    def expand(p: Path): Path = ofPath(p) match {
      case SingletonType(q) => expand(q) // step
      case _ => p // refl
    }
    
    def expand(tp: Type): Type =  tp match {
      case TypeSel(p, a) => member(SingletonType(p), a) match {
        case Some(MType(n, Some(tp))) => expand(tp) // expand-type
        case _ => tp // expand-absttype / expand-class
      }
      case _ => tp // expand-signature / expand-singleton
    }
    
    def <:<(tp1: Type, tp2: Type): Boolean = trace(expand(tp1)+" <:< "+expand(tp2), (expand(tp1), expand(tp2)) match {
      case (x, y) if x==y => true
      case (SingletonType(p), SingletonType(q)) => expand(p) == expand(q)   // <:-singleton-right
      case (SingletonType(p), u) => <:<(ofExpand(p), u)                     // <:-singleton-left
      case (TypeSel(p, a), TypeSel(q, b)) if a==b => expand(p) == expand(q) // <:-paths
      case (TypeSel(p, a), u@TypeSel(_, _)) => member(SingletonType(p), a) match {    // <:-class
        case Some(MTrait(_, TypeSig(parents, _))) => parents.exists(tp => <:<(tp, u))
        case _ => false
      }
      case (TypeSig(parents, _), u@TypeSel(_, _)) => parents.exists(tp => <:<(tp, u)) // <:-sig-left
      case (t, u@TypeSig(parents, mems)) => parents.forall ((parent: Type) => <:<(t, parent)) &&
                                          <:<(t, unfolds(t).get, u, mems) // DEVIATION: oversight in paper (binders do not seem to be in Gamma)?
    })

    // go under two binders: put self variables in context (with their type)
    // then we can just treat the "raw" members -- TODO: enforce this discipline through the type system?
    def <:<(selfTp1: Type, mem1: UnderBinder[Name, List[Member]], selfTp2: Type, mem2: UnderBinder[Name, List[Member]]): Boolean = 
      underBinder(mem1, List(selfTp1)) { (m1: List[Member]) =>
        (.underBinder(mem2, List(selfTp2)) { (m2: List[Member]) => 
           (.<:<(m1, m2))})
      }

    // @pre the binders in mem1, mem2 are in the context now
    def <:<(mem1: Member, mem2: Member): Boolean = trace(mem1+" <:< "+mem2, (mem1, mem2) match {
      case (MField(n1, tp1, v1),MField(n2, tp2, v2))  if n1 == n2 => <:<(tp1, tp2)         // <:-member-field (TODO: any constraints on abstract vs concrete?)
      case (MMethod(n1, formals1, tp1, v1), MMethod(n2, formals2, tp2, v2)) if n1 == n2 => // <:-member-method
        <:<(tp1, tp2) &&  // covariant for return type
        formals2.zip(formals1).forall({case (t2, t1) => <:<(t2, t1)}) // pointwise contravariant for arguments
      case _ => mem1 == mem2  // <:-member-type / <:-member-class
    })
    
    def <:<(mems1: List[Member], mems2: List[Member]): Boolean = mems1.forall(m1 => mems2.exists(m2 => m1.matches(m2) implies <:<(m1,m2)))
      
    def wf(tp: Type): Boolean = tp match {
      case TPUnit() => true
      case SingletonType(p) => 
         wf(ofExpand(p)) // DEVIATION: expansion for consistency
      case TypeSel(p, a) =>
         member(SingletonType(p), a) match {
        case Some(m) => m.isInstanceOf[TypeMember[Type]]// wf-class & wf-type -- DEVIATION: our wf-type doesn't check T wf
         // TODO: use TypeMemberUnapp
        case None => false
      }
      
      case tp: TypeSig => wfSig(tp, tp)
    }

    // WF-X-Signature
    def wfSig(selfT: Type, sig: TypeSig): Boolean = 
      unsequence(sig.members).forall(ubMem => wfMem(ubMem, selfT)) &&
      sig.parents.forall(wf) && {
        var inheritedMems = (for(val parent <- sig.parents) yield(unfolds(parent).get)).toList 
        
        while(!inheritedMems.isEmpty) {
          val tail = inheritedMems.tail
          val head = inheritedMems.head
          
          if(!tail.forall( ub => <:<(sig, merge(ub, sig.members), sig, head))) // TODO: is sig the right type?
						return false
            
          inheritedMems = tail
        }
        true
      }
    
    def wfMem(ubMem: UnderBinder[Name, Member], tp: Type): Boolean = underBinder(ubMem, List(tp))(mem => .wfMem(Path_.fromName(ubMem.scope(0)), mem))
    def wfMem(selfVar: Path, mem: Member) = trace("wfmem("+mem+")", mem match {    
      case MType(_, v) => v.map(wf).get(true)                         // WF-X-Type
      case MField(_, tp, v) => v.map(tm => ofCheck(tm, tp)).get(true) // WF-X-Field
      case MTrait(n, sig) => wfSig(TypeSel(selfVar, n), sig)          // WF-X-Class
      case MMethod(n, formals, tp, b) => wf(tp) && formals.forall(tp => wf(tp)) && // WF-X-Method
        (b match { 
          case Some(body)=>  underBinder(body, formals) { (b: Term) => (.ofCheck(b, tp)) }
          case None => true
        })
    })    

    def merge(as: List[UnderBinder[Name, List[Member]]], b: UnderBinder[Name, List[Member]]): UnderBinder[Name, List[Member]] = 
      as.foldRight(b)(merge) // sweet, sweet FP
      
    /**
     * @pre u.binder.length == tps.length
     */
    def underBinder[s,t](u: UnderBinder[Name, t], tps: List[Type])(f: t => Typer => s): s  = f(u.extract)(extend(u.scope, tps))
    
    def merge(a: UnderBinder[Name, List[Member]], b: UnderBinder[Name, List[Member]]): UnderBinder[Name, List[Member]] = {
      val ab: List[UnderBinder[Name, Member]]= List.concat(unsequence(a),unsequence(b))
      sequence(keepLast(overriddenBy)(ab))
    }

    def concreteMems(mems: Option[UnderBinder[Name, List[Member]]]): Boolean = mems match {
      case Some(mems) => unsequence(mems).forall(concrete)
      case None => false
    }

    // these are the methods that work on tricky UnderBinder stuff
    def overriddenBy(a: UnderBinder[Name,Member], b: UnderBinder[Name, Member]): Boolean = a.extract.matches(b.extract)
    
    def concrete(ubMem: UnderBinder[Name, Member]): Boolean = ubMem.extract.isValue implies ubMem.extract.isConcrete // DEVIATION: only *value* members need be concrete

    // problem is to substitute selfVar (if any) in and get a cloned Member (that doesn't have BoundElement's)
    def getMember(name: String, selfVar: Option[Path], mems: Option[UnderBinder[Name, List[Member]]]): Option[Member] = trace("getMember("+name+", "+selfVar+", "+mems+")", 
     mems match {
      case Some(mems) => unsequence(mems).find(x => x.extract.name == name) match {
          case Some(ubMem) => selfVar match {
            case Some(s) => Some(ubMem.extract(Map(ubMem.scope(0) -> s)))
            case None => Some(ubMem.extract)
          }
          case None => None
        }
      case None => None      
    })
  }
  
  
  // helper methods, should go in Scala libraries?
  // TODO: add to scala.runtime.RichBoolean?
  implicit def myRichBoolean(b: Boolean): MyRichBoolean = new MyRichBoolean(b)
  class  MyRichBoolean(x: Boolean) extends Proxy { def self: Any = x // Proxy.self
    def implies(that: => Boolean): Boolean = (!x) || that  
  }


  def keepLast[a](pred: (a, a) => Boolean)(xs: List[a]): List[a] = takeIfOnTail( ((head: a) => tail => !tail.exists((el: a) => pred(head, el))))(xs)
      
  /** Result is a subset of `xs', constructed by taking every consecutive `el' in `xs' and adding it 
   * to the result if `pred(el, elements after el)' 
   */
  def takeIfOnTail[a](pred: a => List[a] => Boolean)(xs: List[a]): List[a] = {
      var list = xs
      val res = new ListBuffer[a]
                             
      while(!list.isEmpty) {
        val head = list.head
        val tail = list.tail
        
        list = list.tail
        
        if(pred(head)(tail))
          res+=head         
      }
      
      res.toList
    }
  
// indented tracing  
  private var indentCount = 0

  private def indent = indentCount=indentCount+2
  private def deindent = indentCount=indentCount-2
  private def indentPrint(s: String) = {
    val indentStr = List.toString(List.make(indentCount, ' '))
    for(val l <- s lines)
      Console.println(indentStr+l)
  }
  def trace[t](s: String, x: => t): t ={indentPrint(s+"= "); indent; val xx=x; deindent;indentPrint("["+s+"] = "+xx+"\n");xx}
}